Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix two syntax file issues #20

Closed
wants to merge 2 commits into from
Closed

Fix two syntax file issues #20

wants to merge 2 commits into from

Conversation

maxzinkus
Copy link
Contributor

Addresses #17

This may introduce some weird edge cases with nested comments. However, it preserves correct behavior for normal comments and fixes the case of nested comments in a similar way to vim's `c.vim` (using a dedicated region for line comments). As with `c.vim`, we shrug at the edge cases.
@maxzinkus
Copy link
Contributor Author

@mlr-msft 🙂

@maxzinkus
Copy link
Contributor Author

@mlr-msft @SimonForest @fmrl @nikswamy @msprotz @protz anyone want to close this out so I can delete my fork? 🙏

@mtzguido
Copy link
Member

Hello Max, thanks for this. The first commit looks good to me and fixes an old problem. The second one introduces a slight problem though, module paths have their last character not highlighted:
image

I was actually agreeing with your comment here #19 (comment), maybe like this? (remove the me=e-1, allow . in module names, change start of fstarPreDef to [:print:])

diff --git a/syntax/fstar.vim b/syntax/fstar.vim
index f01a3b1..2e607cd 100644
--- a/syntax/fstar.vim
+++ b/syntax/fstar.vim
@@ -114,8 +114,8 @@ syn region   fstarNone matchgroup=fstarKeyword start="\<open\>" matchgroup=fstar
 syn match    fstarKeyword "\<include\>" skipwhite skipempty nextgroup=fstarModParam,fstarFullMod
 
 " "module" - somewhat complicated stuff ;-)
-syn region   fstarModule matchgroup=fstarKeyword start="\<module\>" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>"me=e-1 contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef
-syn region   fstarPreDef start="."me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS
+syn region   fstarModule matchgroup=fstarKeyword start="\<module\>" matchgroup=fstarModule end="\<\u\(\w\|\.\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef
+syn region   fstarPreDef start="[:print:]"me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS
 syn region   fstarModParam start="([^*]" end=")" contained contains=@fstarAENoParen,fstarModParam1,fstarVal
 syn match    fstarModParam1 "\<\u\(\w\|'\)*\>" contained skipwhite skipempty nextgroup=fstarPreMPRestr

That said I'm pretty unfamiliar with these files, so take with a grain of salt.

By the way, we are developing a VSCode extension for F*, so I doubt this repo will see much use. I however do have this installed for syntax highlighting, but I do not use the interactive mode.

@maxzinkus
Copy link
Contributor Author

Ah! Irksome. If you want to snag that first commit in and omit the second, then that's totally fine by me. I've actually not looked at FStar with Vim in a while either 😅

Either way- thanks for following up!

@maxzinkus maxzinkus closed this Mar 24, 2023
@mtzguido
Copy link
Member

Thanks, I pushed your first commit, and my edit of the second mentioning you.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

module syntax line not correctly ended Syntax highlighting is wrong for comments
2 participants